Integrated circuits (ICs) can be implemented to perform a variety of functions. Some ICs can be programmed to perform specified functions. One example of an IC that can be programmed is a field programmable gate array (FPGA). An FPGA typically includes an array of programmable tiles. These programmable tiles can include, for example, input/output blocks (IOBs), configurable logic blocks (CLBs), dedicated random access memory blocks (BRAM), multipliers, digital signal processing blocks (DSPs), processors, clock managers, delay lock loops (DLLs), and so forth.
Each programmable tile typically includes both programmable interconnect circuitry and programmable logic circuitry. The programmable interconnect circuitry typically includes a large number of interconnect lines of varying lengths interconnected by programmable interconnect points (PIPs). The programmable logic circuitry implements the logic of a user design using programmable elements that can include, for example, function generators, registers, arithmetic logic, and so forth.
The programmable interconnect and programmable logic circuitries are typically programmed by loading a stream of configuration data into internal configuration memory cells that define how the programmable elements are configured. The configuration data can be read from memory (e.g., from an external PROM) or written into the FPGA by an external device. The collective states of the individual memory cells then determine the function of the FPGA.
Another type of programmable IC is the complex programmable logic device, or CPLD. A CPLD includes two or more “function blocks” connected together and to input/output (I/O) resources by an interconnect switch matrix. Each function block of the CPLD includes a two-level AND/OR structure similar to those used in programmable logic arrays (PLAs) and programmable array logic (PAL) devices. In CPLDs, configuration data is typically stored on-chip in non-volatile memory. In some CPLDs, configuration data is stored on-chip in non-volatile memory, then downloaded to volatile memory as part of an initial configuration (programming) sequence.
For all of these programmable ICs, the functionality of the device is controlled by data bits provided to the device for that purpose. The data bits can be stored in volatile memory (e.g., static memory cells, as in FPGAs and some CPLDs), in non-volatile memory (e.g., FLASH memory, as in some CPLDs), or in any other type of memory cell.
Other programmable ICs are programmed by applying a processing layer, such as a metal layer, that programmably interconnects the various elements on the device. These programmable ICs are known as mask programmable devices. Programmable ICs can also be implemented in other ways, e.g., using fuse or antifuse technology. The phrase “programmable IC” can include, but is not limited to these devices and further can encompass devices that are only partially programmable. For example, one type of programmable IC includes a combination of hard-coded transistor logic and a programmable switch fabric that programmably interconnects the hard-coded transistor logic.
The process by which a circuit design is implemented within an IC, including a programmable IC, is referred to as “synthesis” or a “synthesis flow.” One example of a synthesis flow begins with a circuit design specified as a collection of one or more hardware description language (HDL) files. The HDL files are processed through several different transformations that collectively form the synthesis flow culminating in a gate level netlist. The various circuit elements of the gate level netlist are correlated with actual circuit blocks or structures available on the particular IC in which the circuit design is to be implemented.
In order to ensure that the output generated by the synthesis flow is equivalent to the input provided, a formal verification process is performed. In general, the formal verification process compares the input to the synthesis flow with the output of the synthesis flow. Formal verification ensures that the output of the synthesis flow correctly implements the specification for the circuit design as does the input to the synthesis flow. Formal verification further can ensure that the input, which is typically specified in a high level or abstract form, is correctly translated into the lower level form. As such, formal verification ensures that the input to the synthesis flow is functionally equivalent to the output of the synthesis flow.
Formal verification, however, is a complex problem. The complexity arises, in large part, from the significant difference between the input to the synthesis flow and the resulting output. In most cases, formal verification is a time consuming process, but possible to perform. In other cases, however, formal verification and, more particularly, establishing equivalency between input and output of the synthesis flow, is not possible.